$\forall$${\it ds}_{1}$, ${\it ds}_{2}$:$a$:Id fp$\rightarrow$ Type, ${\it da}$:$a$:Knd fp$\rightarrow$ Type. effect{-}type(${\it ds}_{1}$;${\it ds}_{2}$;${\it da}$) $\in$ Type